Theorem 3expib 1122

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 1119	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	impd 412	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

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

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 1089

This theorem is referenced by:  3anidm12  1419  mob  3667  eqbrrdva  5816  fcoOLD  6681  f1oiso2  7284  frxp  8039  onfununi  8247  smoel2  8269  smoiso2  8275  3ecoptocl  8674  ssfi  9043  f1domfi  9054  rex2dom  9116  dffi2  9285  elfiun  9292  dif1card  9872  infxpenlem  9875  cfeq0  10118  cfsuc  10119  cfflb  10121  cfslb2n  10130  cofsmo  10131  domtriomlem  10304  axdc3lem4  10315  axdc4lem  10317  ttukey2g  10378  tskxpss  10634  grudomon  10679  elnpi  10850  dedekind  11244  nn0n0n1ge2b  12407  fzind  12524  suprzcl2  12784  icoshft  13311  fzen  13379  hashgt23el  14244  hashbclem  14269  seqcoll  14283  relexpsucl  14842  relexpsucr  14843  relexpfld  14860  shftuz  14880  mulgcd  16356  algcvga  16382  lcmneg  16406  ressbas  17045  ressbasOLD  17046  resseqnbas  17049  resslemOLD  17050  ressress  17056  psss  18396  tsrlemax  18402  isnmgm  18428  gsummgmpropd  18463  iscmnd  19495  ring1ne0  19925  unitmulclb  20002  isdrngd  20121  issrngd  20227  rmodislmodlem  20296  rmodislmod  20297  rmodislmodOLD  20298  abvn0b  20679  isphld  20965  mpfaddcl  21421  mpfmulcl  21422  pf1addcl  21625  pf1mulcl  21626  fitop  22155  hausnei2  22610  ordtt1  22636  locfincmp  22783  basqtop  22968  filfi  23116  fgcl  23135  neifil  23137  filuni  23142  cnextcn  23324  prdsmet  23629  blssps  23683  blss  23684  metcnp3  23802  hlhil  24713  volsup2  24875  sincosq1sgn  25761  sincosq2sgn  25762  sincosq3sgn  25763  sincosq4sgn  25764  sinq12ge0  25771  bcmono  26531  iswlkg  28269  umgrwwlks2on  28610  clwlkclwwlkfo  28661  3cyclfrgrrn1  28937  grpodivf  29188  ipf  29363  shintcli  29979  spanuni  30194  adjadj  30586  unopadj2  30588  hmopadj  30589  hmopbdoptHIL  30638  resvsca  31823  resvlem  31824  resvlemOLD  31825  submateq  32055  esumcocn  32344  bnj1379  33107  bnj571  33183  bnj594  33189  bnj580  33190  bnj600  33196  bnj1189  33286  bnj1321  33304  bnj1384  33309  f1resrcmplf1dlem  33355  hashfundm  33371  cplgredgex  33379  cusgr3cyclex  33395  loop1cycl  33396  umgr2cycllem  33399  umgr2cycl  33400  acycgr2v  33409  cusgracyclt3v  33415  climuzcnv  33926  fness  34675  bj-idreseq  35487  bj-imdiridlem  35510  neificl  36065  metf1o  36067  isismty  36113  ismtybndlem  36118  ablo4pnp  36192  divrngcl  36269  keridl  36344  prnc  36379  lsmsatcv  37326  llncvrlpln2  37874  lplncvrlvol2  37932  linepsubN  38069  pmapsub  38085  dalawlem10  38197  dalawlem13  38200  dalawlem14  38201  dalaw  38203  diaf11N  39366  dibf11N  39478  ismrcd1  40831  ismrcd2  40832  mzpincl  40867  mzpadd  40871  mzpmul  40872  pellfundge  41015  imasgim  41237  sqrtcval  41620  stoweidlem2  43929  stoweidlem17  43944  imaelsetpreimafv  45263  opnneir  46616  i0oii  46629  io1ii  46630