Theorem 3expib 1123

Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.)

Hypothesis

Ref	Expression
3exp.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
3expib	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Proof of Theorem 3expib

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3exp 1120	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 412	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 398  df-3an 1090

This theorem is referenced by:  3anidm12  1420  mob  3714  eqbrrdva  5870  fcoOLD  6743  f1oiso2  7349  frxp  8112  onfununi  8341  smoel2  8363  smoiso2  8369  3ecoptocl  8803  ssfi  9173  f1domfi  9184  rex2dom  9246  dffi2  9418  elfiun  9425  dif1card  10005  infxpenlem  10008  cfeq0  10251  cfsuc  10252  cfflb  10254  cfslb2n  10263  cofsmo  10264  domtriomlem  10437  axdc3lem4  10448  axdc4lem  10450  ttukey2g  10511  tskxpss  10767  grudomon  10812  elnpi  10983  dedekind  11377  nn0n0n1ge2b  12540  fzind  12660  suprzcl2  12922  icoshft  13450  fzen  13518  hashgt23el  14384  hashfundm  14402  hashbclem  14411  seqcoll  14425  relexpsucl  14978  relexpsucr  14979  relexpfld  14996  shftuz  15016  mulgcd  16490  algcvga  16516  lcmneg  16540  ressbas  17179  ressbasOLD  17180  resseqnbas  17186  resslemOLD  17187  ressress  17193  psss  18533  tsrlemax  18539  isnmgm  18565  gsummgmpropd  18600  issgrpd  18621  iscmnd  19662  ring1ne0  20111  unitmulclb  20195  isdrngd  20390  isdrngdOLD  20392  issrngd  20469  rmodislmodlem  20539  rmodislmod  20540  rmodislmodOLD  20541  abvn0b  20920  isphld  21207  mpfaddcl  21668  mpfmulcl  21669  pf1addcl  21872  pf1mulcl  21873  fitop  22402  hausnei2  22857  ordtt1  22883  locfincmp  23030  basqtop  23215  filfi  23363  fgcl  23382  neifil  23384  filuni  23389  cnextcn  23571  prdsmet  23876  blssps  23930  blss  23931  metcnp3  24049  hlhil  24960  volsup2  25122  sincosq1sgn  26008  sincosq2sgn  26009  sincosq3sgn  26010  sincosq4sgn  26011  sinq12ge0  26018  bcmono  26780  iswlkg  28870  umgrwwlks2on  29211  clwlkclwwlkfo  29262  3cyclfrgrrn1  29538  grpodivf  29791  ipf  29966  shintcli  30582  spanuni  30797  adjadj  31189  unopadj2  31191  hmopadj  31192  hmopbdoptHIL  31241  resvsca  32444  resvlem  32445  resvlemOLD  32446  submateq  32789  esumcocn  33078  bnj1379  33841  bnj571  33917  bnj594  33923  bnj580  33924  bnj600  33930  bnj1189  34020  bnj1321  34038  bnj1384  34043  f1resrcmplf1dlem  34089  cplgredgex  34111  cusgr3cyclex  34127  loop1cycl  34128  umgr2cycllem  34131  umgr2cycl  34132  acycgr2v  34141  cusgracyclt3v  34147  climuzcnv  34656  mpomulcn  35162  fness  35234  bj-idreseq  36043  bj-imdiridlem  36066  neificl  36621  metf1o  36623  isismty  36669  ismtybndlem  36674  ablo4pnp  36748  divrngcl  36825  keridl  36900  prnc  36935  lsmsatcv  37880  llncvrlpln2  38428  lplncvrlvol2  38486  linepsubN  38623  pmapsub  38639  dalawlem10  38751  dalawlem13  38754  dalawlem14  38755  dalaw  38757  diaf11N  39920  dibf11N  40032  ismrcd1  41436  ismrcd2  41437  mzpincl  41472  mzpadd  41476  mzpmul  41477  pellfundge  41620  imasgim  41842  sqrtcval  42392  stoweidlem2  44718  stoweidlem17  44733  imaelsetpreimafv  46063  opnneir  47539  i0oii  47552  io1ii  47553